(1
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 86)
  ("(var3 stable)" 86 332)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 90)
  ("(var4 stable)" 90 210)
  ("(var4 down)" 210 283)
  ("(var4 stable)" 283 285)
  ("(var4 down)" 285 287)
  ("(var4 stable)" 287 330)
  ("(var4 down)" 330 332)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 49)
  ("(var1 down)" 49 51)
  ("(var1 up)" 51 88)
  ("(var1 stable)" 88 332)
  ("(var2 stable)" 0 73)
  ("(var2 down)" 73 75)
  ("(var2 up)" 75 191)
  ("(var2 stable)" 191 332)
 )
)
(2
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 65)
  ("(var3 stable)" 65 294)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 37)
  ("(var4 down)" 37 39)
  ("(var4 up)" 39 71)
  ("(var4 stable)" 71 152)
  ("(var4 down)" 152 249)
  ("(var4 stable)" 249 252)
  ("(var4 down)" 252 258)
  ("(var4 stable)" 258 294)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 66)
  ("(var1 stable)" 66 294)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 up)" 55 173)
  ("(var2 down)" 173 175)
  ("(var2 stable)" 175 294)
 )
)
(3
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 108)
  ("(var3 stable)" 108 340)
  ("(var4 stable)" 0 78)
  ("(var4 up)" 78 110)
  ("(var4 stable)" 110 112)
  ("(var4 up)" 112 115)
  ("(var4 stable)" 115 199)
  ("(var4 down)" 199 296)
  ("(var4 stable)" 296 340)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 105)
  ("(var1 stable)" 105 107)
  ("(var1 up)" 107 109)
  ("(var1 stable)" 109 340)
  ("(var2 stable)" 0 97)
  ("(var2 down)" 97 99)
  ("(var2 stable)" 99 132)
  ("(var2 up)" 132 194)
  ("(var2 down)" 194 196)
  ("(var2 up)" 196 227)
  ("(var2 stable)" 227 340)
 )
)
(4
 (
  ("(var3 stable)" 0 72)
  ("(var3 up)" 72 101)
  ("(var3 stable)" 101 321)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 96)
  ("(var4 stable)" 96 99)
  ("(var4 up)" 99 103)
  ("(var4 stable)" 103 215)
  ("(var4 down)" 215 280)
  ("(var4 stable)" 280 321)
  ("(var1 stable)" 0 72)
  ("(var1 down)" 72 74)
  ("(var1 up)" 74 101)
  ("(var1 down)" 101 103)
  ("(var1 stable)" 103 321)
  ("(var2 stable)" 0 90)
  ("(var2 down)" 90 92)
  ("(var2 up)" 92 224)
  ("(var2 stable)" 224 321)
 )
)
(5
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 110)
  ("(var3 stable)" 110 343)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 113)
  ("(var4 stable)" 113 208)
  ("(var4 down)" 208 298)
  ("(var4 stable)" 298 301)
  ("(var4 down)" 301 303)
  ("(var4 stable)" 303 343)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 87)
  ("(var1 stable)" 87 89)
  ("(var1 up)" 89 113)
  ("(var1 stable)" 113 115)
  ("(var1 up)" 115 117)
  ("(var1 stable)" 117 343)
  ("(var2 stable)" 0 103)
  ("(var2 down)" 103 105)
  ("(var2 stable)" 105 139)
  ("(var2 up)" 139 235)
  ("(var2 down)" 235 237)
  ("(var2 stable)" 237 241)
  ("(var2 up)" 241 243)
  ("(var2 stable)" 243 343)
 )
)
(6
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 95)
  ("(var3 stable)" 95 340)
  ("(var4 stable)" 0 65)
  ("(var4 up)" 65 92)
  ("(var4 stable)" 92 222)
  ("(var4 down)" 222 224)
  ("(var4 up)" 224 226)
  ("(var4 down)" 226 292)
  ("(var4 stable)" 292 340)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 55)
  ("(var1 down)" 55 57)
  ("(var1 up)" 57 60)
  ("(var1 stable)" 60 62)
  ("(var1 up)" 62 96)
  ("(var1 stable)" 96 340)
  ("(var2 stable)" 0 82)
  ("(var2 down)" 82 84)
  ("(var2 stable)" 84 125)
  ("(var2 up)" 125 127)
  ("(var2 stable)" 127 130)
  ("(var2 up)" 130 231)
  ("(var2 stable)" 231 340)
 )
)
(7
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 96)
  ("(var3 stable)" 96 99)
  ("(var3 up)" 99 101)
  ("(var3 stable)" 101 325)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 101)
  ("(var4 stable)" 101 189)
  ("(var4 down)" 189 281)
  ("(var4 stable)" 281 325)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 97)
  ("(var1 stable)" 97 325)
  ("(var2 stable)" 0 87)
  ("(var2 down)" 87 89)
  ("(var2 up)" 89 224)
  ("(var2 stable)" 224 325)
 )
)
(8
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 87)
  ("(var3 stable)" 87 344)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 97)
  ("(var4 stable)" 97 198)
  ("(var4 down)" 198 200)
  ("(var4 up)" 200 202)
  ("(var4 down)" 202 230)
  ("(var4 up)" 230 232)
  ("(var4 down)" 232 301)
  ("(var4 up)" 301 303)
  ("(var4 down)" 303 305)
  ("(var4 stable)" 305 344)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 91)
  ("(var1 stable)" 91 344)
  ("(var2 stable)" 0 78)
  ("(var2 down)" 78 80)
  ("(var2 stable)" 80 124)
  ("(var2 up)" 124 226)
  ("(var2 stable)" 226 344)
 )
)
(9
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 55)
  ("(var3 stable)" 55 57)
  ("(var3 up)" 57 80)
  ("(var3 stable)" 80 299)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 79)
  ("(var4 down)" 79 81)
  ("(var4 stable)" 81 155)
  ("(var4 down)" 155 266)
  ("(var4 stable)" 266 299)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 77)
  ("(var1 stable)" 77 299)
  ("(var2 stable)" 0 68)
  ("(var2 down)" 68 70)
  ("(var2 up)" 70 196)
  ("(var2 stable)" 196 299)
 )
)
(10
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 110)
  ("(var3 stable)" 110 336)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 113)
  ("(var4 stable)" 113 222)
  ("(var4 down)" 222 292)
  ("(var4 stable)" 292 336)
  ("(var1 stable)" 0 83)
  ("(var1 up)" 83 113)
  ("(var1 stable)" 113 336)
  ("(var2 stable)" 0 135)
  ("(var2 up)" 135 204)
  ("(var2 down)" 204 206)
  ("(var2 up)" 206 237)
  ("(var2 stable)" 237 336)
 )
)
(11
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 87)
  ("(var3 stable)" 87 306)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 88)
  ("(var4 stable)" 88 169)
  ("(var4 down)" 169 264)
  ("(var4 stable)" 264 306)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 83)
  ("(var1 stable)" 83 306)
  ("(var2 stable)" 0 75)
  ("(var2 down)" 75 77)
  ("(var2 up)" 77 116)
  ("(var2 stable)" 116 118)
  ("(var2 up)" 118 199)
  ("(var2 stable)" 199 306)
 )
)
(12
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 67)
  ("(var3 stable)" 67 304)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 72)
  ("(var4 stable)" 72 171)
  ("(var4 down)" 171 259)
  ("(var4 up)" 259 261)
  ("(var4 down)" 261 263)
  ("(var4 stable)" 263 304)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 71)
  ("(var1 stable)" 71 73)
  ("(var1 up)" 73 77)
  ("(var1 stable)" 77 304)
  ("(var2 stable)" 0 58)
  ("(var2 down)" 58 60)
  ("(var2 up)" 60 192)
  ("(var2 stable)" 192 304)
 )
)
(13
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 72)
  ("(var3 stable)" 72 285)
  ("(var4 stable)" 0 44)
  ("(var4 up)" 44 78)
  ("(var4 stable)" 78 160)
  ("(var4 up)" 160 163)
  ("(var4 down)" 163 165)
  ("(var4 stable)" 165 167)
  ("(var4 down)" 167 237)
  ("(var4 up)" 237 239)
  ("(var4 down)" 239 243)
  ("(var4 stable)" 243 285)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 69)
  ("(var1 stable)" 69 285)
  ("(var2 stable)" 0 55)
  ("(var2 up)" 55 57)
  ("(var2 down)" 57 62)
  ("(var2 up)" 62 185)
  ("(var2 stable)" 185 285)
 )
)
(14
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 105)
  ("(var3 stable)" 105 335)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 111)
  ("(var4 stable)" 111 194)
  ("(var4 down)" 194 228)
  ("(var4 up)" 228 230)
  ("(var4 down)" 230 290)
  ("(var4 stable)" 290 335)
  ("(var1 stable)" 0 75)
  ("(var1 up)" 75 103)
  ("(var1 stable)" 103 333)
  ("(var1 down)" 333 335)
  ("(var2 stable)" 0 95)
  ("(var2 down)" 95 97)
  ("(var2 up)" 97 196)
  ("(var2 down)" 196 198)
  ("(var2 up)" 198 227)
  ("(var2 stable)" 227 335)
 )
)
(15
 (
  ("(var3 up)" 0 2)
  ("(var3 down)" 2 4)
  ("(var3 stable)" 4 54)
  ("(var3 up)" 54 78)
  ("(var3 stable)" 78 286)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 96)
  ("(var4 stable)" 96 167)
  ("(var4 down)" 167 251)
  ("(var4 stable)" 251 281)
  ("(var4 up)" 281 284)
  ("(var4 down)" 284 286)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 85)
  ("(var1 stable)" 85 286)
  ("(var2 stable)" 0 104)
  ("(var2 up)" 104 190)
  ("(var2 stable)" 190 286)
 )
)
(16
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 52)
  ("(var3 stable)" 52 54)
  ("(var3 up)" 54 80)
  ("(var3 stable)" 80 317)
  ("(var4 stable)" 0 52)
  ("(var4 up)" 52 80)
  ("(var4 down)" 80 82)
  ("(var4 up)" 82 84)
  ("(var4 stable)" 84 184)
  ("(var4 down)" 184 273)
  ("(var4 stable)" 273 317)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 81)
  ("(var1 stable)" 81 317)
  ("(var2 stable)" 0 70)
  ("(var2 down)" 70 72)
  ("(var2 stable)" 72 106)
  ("(var2 up)" 106 202)
  ("(var2 stable)" 202 317)
 )
)
(17
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 83)
  ("(var3 stable)" 83 85)
  ("(var3 up)" 85 106)
  ("(var3 down)" 106 108)
  ("(var3 stable)" 108 348)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 106)
  ("(var4 stable)" 106 110)
  ("(var4 up)" 110 112)
  ("(var4 stable)" 112 208)
  ("(var4 down)" 208 310)
  ("(var4 stable)" 310 348)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 109)
  ("(var1 stable)" 109 348)
  ("(var2 stable)" 0 96)
  ("(var2 down)" 96 98)
  ("(var2 stable)" 98 139)
  ("(var2 up)" 139 240)
  ("(var2 stable)" 240 348)
 )
)
(18
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 95)
  ("(var3 stable)" 95 334)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 92)
  ("(var4 stable)" 92 98)
  ("(var4 up)" 98 100)
  ("(var4 stable)" 100 212)
  ("(var4 down)" 212 288)
  ("(var4 stable)" 288 334)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 94)
  ("(var1 stable)" 94 334)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 85)
  ("(var2 up)" 85 187)
  ("(var2 stable)" 187 190)
  ("(var2 up)" 190 226)
  ("(var2 stable)" 226 334)
 )
)
(19
 (
  ("(var3 down)" 0 4)
  ("(var3 stable)" 4 42)
  ("(var3 up)" 42 78)
  ("(var3 stable)" 78 307)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 73)
  ("(var4 stable)" 73 170)
  ("(var4 down)" 170 277)
  ("(var4 stable)" 277 307)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 71)
  ("(var1 stable)" 71 307)
  ("(var2 stable)" 0 60)
  ("(var2 down)" 60 62)
  ("(var2 up)" 62 188)
  ("(var2 down)" 188 193)
  ("(var2 stable)" 193 307)
 )
)
(20
 (
  ("(var3 stable)" 0 27)
  ("(var3 up)" 27 60)
  ("(var3 stable)" 60 277)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 63)
  ("(var4 stable)" 63 167)
  ("(var4 down)" 167 238)
  ("(var4 stable)" 238 277)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 62)
  ("(var1 stable)" 62 64)
  ("(var1 up)" 64 68)
  ("(var1 stable)" 68 277)
  ("(var2 stable)" 0 54)
  ("(var2 down)" 54 56)
  ("(var2 up)" 56 166)
  ("(var2 down)" 166 168)
  ("(var2 up)" 168 170)
  ("(var2 stable)" 170 277)
 )
)
(21
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 105)
  ("(var3 stable)" 105 321)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 109)
  ("(var4 stable)" 109 184)
  ("(var4 down)" 184 186)
  ("(var4 stable)" 186 189)
  ("(var4 up)" 189 191)
  ("(var4 down)" 191 276)
  ("(var4 stable)" 276 321)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 100)
  ("(var1 stable)" 100 321)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 94)
  ("(var2 up)" 94 217)
  ("(var2 stable)" 217 321)
 )
)
(22
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 77)
  ("(var3 stable)" 77 310)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 74)
  ("(var4 stable)" 74 76)
  ("(var4 up)" 76 78)
  ("(var4 stable)" 78 168)
  ("(var4 down)" 168 289)
  ("(var4 stable)" 289 310)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 81)
  ("(var1 stable)" 81 310)
  ("(var2 stable)" 0 67)
  ("(var2 down)" 67 69)
  ("(var2 up)" 69 203)
  ("(var2 stable)" 203 310)
 )
)
(23
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 83)
  ("(var3 stable)" 83 86)
  ("(var3 up)" 86 88)
  ("(var3 stable)" 88 329)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 88)
  ("(var4 stable)" 88 205)
  ("(var4 down)" 205 216)
  ("(var4 stable)" 216 218)
  ("(var4 up)" 218 220)
  ("(var4 down)" 220 289)
  ("(var4 stable)" 289 323)
  ("(var4 up)" 323 325)
  ("(var4 down)" 325 327)
  ("(var4 up)" 327 329)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 42)
  ("(var1 down)" 42 44)
  ("(var1 up)" 44 79)
  ("(var1 stable)" 79 329)
  ("(var2 stable)" 0 70)
  ("(var2 down)" 70 72)
  ("(var2 up)" 72 192)
  ("(var2 down)" 192 194)
  ("(var2 up)" 194 196)
  ("(var2 stable)" 196 329)
 )
)
(24
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 59)
  ("(var3 stable)" 59 61)
  ("(var3 up)" 61 80)
  ("(var3 stable)" 80 295)
  ("(var4 stable)" 0 53)
  ("(var4 down)" 53 56)
  ("(var4 up)" 56 85)
  ("(var4 stable)" 85 91)
  ("(var4 up)" 91 93)
  ("(var4 stable)" 93 176)
  ("(var4 down)" 176 250)
  ("(var4 up)" 250 252)
  ("(var4 stable)" 252 295)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 81)
  ("(var1 stable)" 81 295)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 74)
  ("(var2 stable)" 74 105)
  ("(var2 up)" 105 204)
  ("(var2 stable)" 204 295)
 )
)
(25
 (
  ("(var3 stable)" 0 25)
  ("(var3 up)" 25 58)
  ("(var3 stable)" 58 290)
  ("(var4 up)" 0 2)
  ("(var4 stable)" 2 35)
  ("(var4 up)" 35 63)
  ("(var4 stable)" 63 65)
  ("(var4 up)" 65 67)
  ("(var4 stable)" 67 155)
  ("(var4 down)" 155 244)
  ("(var4 stable)" 244 290)
  ("(var1 stable)" 0 33)
  ("(var1 up)" 33 58)
  ("(var1 down)" 58 60)
  ("(var1 stable)" 60 290)
  ("(var2 stable)" 0 49)
  ("(var2 down)" 49 51)
  ("(var2 up)" 51 188)
  ("(var2 stable)" 188 290)
 )
)
(26
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 93)
  ("(var3 stable)" 93 343)
  ("(var4 stable)" 0 62)
  ("(var4 down)" 62 64)
  ("(var4 up)" 64 97)
  ("(var4 down)" 97 99)
  ("(var4 up)" 99 101)
  ("(var4 stable)" 101 103)
  ("(var4 up)" 103 105)
  ("(var4 stable)" 105 190)
  ("(var4 down)" 190 193)
  ("(var4 up)" 193 195)
  ("(var4 stable)" 195 220)
  ("(var4 down)" 220 224)
  ("(var4 up)" 224 226)
  ("(var4 stable)" 226 228)
  ("(var4 down)" 228 302)
  ("(var4 stable)" 302 343)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 95)
  ("(var1 stable)" 95 343)
  ("(var2 stable)" 0 86)
  ("(var2 down)" 86 88)
  ("(var2 stable)" 88 128)
  ("(var2 up)" 128 224)
  ("(var2 stable)" 224 343)
 )
)
(27
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 84)
  ("(var3 stable)" 84 87)
  ("(var3 up)" 87 95)
  ("(var3 stable)" 95 97)
  ("(var3 up)" 97 121)
  ("(var3 stable)" 121 372)
  ("(var4 stable)" 0 92)
  ("(var4 up)" 92 135)
  ("(var4 stable)" 135 250)
  ("(var4 down)" 250 329)
  ("(var4 up)" 329 331)
  ("(var4 stable)" 331 372)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 120)
  ("(var1 stable)" 120 122)
  ("(var1 up)" 122 124)
  ("(var1 down)" 124 126)
  ("(var1 up)" 126 128)
  ("(var1 stable)" 128 372)
  ("(var2 stable)" 0 110)
  ("(var2 down)" 110 112)
  ("(var2 stable)" 112 152)
  ("(var2 up)" 152 258)
  ("(var2 stable)" 258 372)
 )
)
(28
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 108)
  ("(var3 stable)" 108 345)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 119)
  ("(var4 stable)" 119 230)
  ("(var4 down)" 230 307)
  ("(var4 stable)" 307 345)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 113)
  ("(var1 stable)" 113 345)
  ("(var2 stable)" 0 97)
  ("(var2 down)" 97 99)
  ("(var2 up)" 99 234)
  ("(var2 stable)" 234 345)
 )
)
(29
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 86)
  ("(var3 stable)" 86 327)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 95)
  ("(var4 stable)" 95 184)
  ("(var4 down)" 184 291)
  ("(var4 stable)" 291 327)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 82)
  ("(var1 stable)" 82 327)
  ("(var2 stable)" 0 71)
  ("(var2 down)" 71 73)
  ("(var2 up)" 73 116)
  ("(var2 down)" 116 119)
  ("(var2 up)" 119 170)
  ("(var2 down)" 170 174)
  ("(var2 up)" 174 208)
  ("(var2 stable)" 208 327)
 )
)
(30
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 90)
  ("(var3 stable)" 90 92)
  ("(var3 up)" 92 94)
  ("(var3 stable)" 94 314)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 90)
  ("(var4 stable)" 90 92)
  ("(var4 up)" 92 94)
  ("(var4 stable)" 94 191)
  ("(var4 down)" 191 284)
  ("(var4 stable)" 284 314)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 65)
  ("(var1 stable)" 65 67)
  ("(var1 up)" 67 92)
  ("(var1 stable)" 92 314)
  ("(var2 stable)" 0 82)
  ("(var2 down)" 82 84)
  ("(var2 up)" 84 205)
  ("(var2 down)" 205 207)
  ("(var2 stable)" 207 314)
 )
)
(31
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 118)
  ("(var3 stable)" 118 369)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 120)
  ("(var4 down)" 120 123)
  ("(var4 stable)" 123 232)
  ("(var4 down)" 232 322)
  ("(var4 up)" 322 325)
  ("(var4 stable)" 325 369)
  ("(var1 stable)" 0 85)
  ("(var1 up)" 85 121)
  ("(var1 stable)" 121 369)
  ("(var2 stable)" 0 104)
  ("(var2 up)" 104 107)
  ("(var2 down)" 107 111)
  ("(var2 up)" 111 250)
  ("(var2 down)" 250 253)
  ("(var2 stable)" 253 369)
 )
)
(32
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 66)
  ("(var3 stable)" 66 322)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 64)
  ("(var4 down)" 64 66)
  ("(var4 up)" 66 72)
  ("(var4 stable)" 72 174)
  ("(var4 down)" 174 278)
  ("(var4 stable)" 278 318)
  ("(var4 up)" 318 320)
  ("(var4 down)" 320 322)
  ("(var1 stable)" 0 30)
  ("(var1 up)" 30 72)
  ("(var1 stable)" 72 322)
  ("(var2 stable)" 0 57)
  ("(var2 down)" 57 59)
  ("(var2 up)" 59 200)
  ("(var2 stable)" 200 322)
 )
)
(33
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 103)
  ("(var3 stable)" 103 333)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 105)
  ("(var4 stable)" 105 208)
  ("(var4 down)" 208 210)
  ("(var4 up)" 210 212)
  ("(var4 down)" 212 298)
  ("(var4 stable)" 298 300)
  ("(var4 down)" 300 302)
  ("(var4 stable)" 302 333)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 104)
  ("(var1 stable)" 104 333)
  ("(var2 stable)" 0 98)
  ("(var2 up)" 98 139)
  ("(var2 down)" 139 141)
  ("(var2 up)" 141 192)
  ("(var2 stable)" 192 194)
  ("(var2 up)" 194 233)
  ("(var2 stable)" 233 333)
 )
)
(34
 (
  ("(var3 stable)" 0 84)
  ("(var3 up)" 84 118)
  ("(var3 stable)" 118 352)
  ("(var4 stable)" 0 89)
  ("(var4 up)" 89 119)
  ("(var4 down)" 119 121)
  ("(var4 stable)" 121 208)
  ("(var4 down)" 208 311)
  ("(var4 stable)" 311 352)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 120)
  ("(var1 stable)" 120 352)
  ("(var2 stable)" 0 107)
  ("(var2 down)" 107 109)
  ("(var2 up)" 109 237)
  ("(var2 stable)" 237 352)
 )
)
(35
 (
  ("(var3 stable)" 0 71)
  ("(var3 down)" 71 74)
  ("(var3 up)" 74 103)
  ("(var3 stable)" 103 317)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 103)
  ("(var4 stable)" 103 183)
  ("(var4 down)" 183 270)
  ("(var4 up)" 270 272)
  ("(var4 down)" 272 274)
  ("(var4 stable)" 274 317)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 100)
  ("(var1 stable)" 100 317)
  ("(var2 stable)" 0 89)
  ("(var2 down)" 89 93)
  ("(var2 up)" 93 95)
  ("(var2 down)" 95 98)
  ("(var2 up)" 98 189)
  ("(var2 stable)" 189 317)
 )
)
(36
 (
  ("(var3 stable)" 0 71)
  ("(var3 down)" 71 73)
  ("(var3 up)" 73 98)
  ("(var3 stable)" 98 332)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 113)
  ("(var4 down)" 113 115)
  ("(var4 stable)" 115 208)
  ("(var4 down)" 208 287)
  ("(var4 stable)" 287 332)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 104)
  ("(var1 stable)" 104 332)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 94)
  ("(var2 stable)" 94 122)
  ("(var2 up)" 122 223)
  ("(var2 stable)" 223 332)
 )
)
(37
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 70)
  ("(var3 stable)" 70 287)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 67)
  ("(var4 stable)" 67 151)
  ("(var4 up)" 151 153)
  ("(var4 down)" 153 240)
  ("(var4 stable)" 240 285)
  ("(var4 down)" 285 287)
  ("(var1 stable)" 0 40)
  ("(var1 up)" 40 70)
  ("(var1 stable)" 70 287)
  ("(var2 stable)" 0 57)
  ("(var2 down)" 57 59)
  ("(var2 stable)" 59 85)
  ("(var2 up)" 85 150)
  ("(var2 stable)" 150 155)
  ("(var2 up)" 155 157)
  ("(var2 stable)" 157 287)
 )
)
(38
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 93)
  ("(var3 stable)" 93 306)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 93)
  ("(var4 stable)" 93 173)
  ("(var4 down)" 173 263)
  ("(var4 stable)" 263 306)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 65)
  ("(var1 stable)" 65 67)
  ("(var1 up)" 67 89)
  ("(var1 stable)" 89 306)
  ("(var2 stable)" 0 79)
  ("(var2 down)" 79 83)
  ("(var2 up)" 83 119)
  ("(var2 stable)" 119 121)
  ("(var2 up)" 121 169)
  ("(var2 down)" 169 171)
  ("(var2 up)" 171 205)
  ("(var2 stable)" 205 306)
 )
)
(39
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 101)
  ("(var3 stable)" 101 356)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 69)
  ("(var4 stable)" 69 74)
  ("(var4 up)" 74 103)
  ("(var4 stable)" 103 233)
  ("(var4 down)" 233 308)
  ("(var4 stable)" 308 315)
  ("(var4 down)" 315 317)
  ("(var4 stable)" 317 356)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 111)
  ("(var1 stable)" 111 356)
  ("(var2 stable)" 0 94)
  ("(var2 down)" 94 96)
  ("(var2 up)" 96 138)
  ("(var2 down)" 138 140)
  ("(var2 up)" 140 236)
  ("(var2 stable)" 236 354)
  ("(var2 down)" 354 356)
 )
)
(40
 (
  ("(var3 stable)" 0 101)
  ("(var3 up)" 101 104)
  ("(var3 stable)" 104 106)
  ("(var3 up)" 106 130)
  ("(var3 stable)" 130 383)
  ("(var4 stable)" 0 103)
  ("(var4 up)" 103 136)
  ("(var4 stable)" 136 262)
  ("(var4 down)" 262 349)
  ("(var4 stable)" 349 383)
  ("(var1 stable)" 0 102)
  ("(var1 up)" 102 133)
  ("(var1 down)" 133 135)
  ("(var1 stable)" 135 383)
  ("(var2 stable)" 0 123)
  ("(var2 down)" 123 125)
  ("(var2 up)" 125 277)
  ("(var2 stable)" 277 383)
 )
)
(41
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 110)
  ("(var3 stable)" 110 329)
  ("(var4 stable)" 0 84)
  ("(var4 up)" 84 114)
  ("(var4 stable)" 114 222)
  ("(var4 down)" 222 292)
  ("(var4 stable)" 292 329)
  ("(var1 stable)" 0 89)
  ("(var1 up)" 89 111)
  ("(var1 stable)" 111 329)
  ("(var2 stable)" 0 103)
  ("(var2 down)" 103 105)
  ("(var2 up)" 105 225)
  ("(var2 down)" 225 228)
  ("(var2 up)" 228 232)
  ("(var2 down)" 232 234)
  ("(var2 up)" 234 236)
  ("(var2 stable)" 236 329)
 )
)
(42
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 104)
  ("(var3 stable)" 104 363)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 111)
  ("(var4 stable)" 111 114)
  ("(var4 up)" 114 116)
  ("(var4 stable)" 116 215)
  ("(var4 down)" 215 315)
  ("(var4 up)" 315 317)
  ("(var4 down)" 317 320)
  ("(var4 stable)" 320 363)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 108)
  ("(var1 stable)" 108 111)
  ("(var1 up)" 111 113)
  ("(var1 stable)" 113 363)
  ("(var2 stable)" 0 96)
  ("(var2 down)" 96 98)
  ("(var2 stable)" 98 138)
  ("(var2 up)" 138 246)
  ("(var2 stable)" 246 363)
 )
)
(43
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 117)
  ("(var3 stable)" 117 363)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 86)
  ("(var4 stable)" 86 89)
  ("(var4 up)" 89 124)
  ("(var4 stable)" 124 223)
  ("(var4 down)" 223 324)
  ("(var4 stable)" 324 363)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 113)
  ("(var1 stable)" 113 363)
  ("(var2 stable)" 0 104)
  ("(var2 down)" 104 108)
  ("(var2 up)" 108 247)
  ("(var2 stable)" 247 363)
 )
)
(44
 (
  ("(var3 stable)" 0 77)
  ("(var3 up)" 77 104)
  ("(var3 stable)" 104 332)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 120)
  ("(var4 stable)" 120 200)
  ("(var4 down)" 200 288)
  ("(var4 up)" 288 290)
  ("(var4 down)" 290 294)
  ("(var4 stable)" 294 332)
  ("(var1 stable)" 0 80)
  ("(var1 up)" 80 82)
  ("(var1 down)" 82 84)
  ("(var1 up)" 84 110)
  ("(var1 stable)" 110 332)
  ("(var2 stable)" 0 101)
  ("(var2 up)" 101 203)
  ("(var2 stable)" 203 242)
  ("(var2 down)" 242 244)
  ("(var2 stable)" 244 332)
 )
)
(45
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 70)
  ("(var3 stable)" 70 308)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 74)
  ("(var4 stable)" 74 196)
  ("(var4 down)" 196 264)
  ("(var4 stable)" 264 308)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 73)
  ("(var1 stable)" 73 308)
  ("(var2 stable)" 0 61)
  ("(var2 down)" 61 66)
  ("(var2 up)" 66 103)
  ("(var2 stable)" 103 105)
  ("(var2 up)" 105 200)
  ("(var2 stable)" 200 308)
 )
)
(46
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 75)
  ("(var3 up)" 75 104)
  ("(var3 stable)" 104 106)
  ("(var3 up)" 106 108)
  ("(var3 stable)" 108 355)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 77)
  ("(var4 down)" 77 79)
  ("(var4 up)" 79 106)
  ("(var4 stable)" 106 209)
  ("(var4 down)" 209 302)
  ("(var4 stable)" 302 304)
  ("(var4 down)" 304 306)
  ("(var4 stable)" 306 355)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 109)
  ("(var1 stable)" 109 355)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 96)
  ("(var2 stable)" 96 139)
  ("(var2 up)" 139 141)
  ("(var2 stable)" 141 143)
  ("(var2 up)" 143 221)
  ("(var2 stable)" 221 355)
 )
)
(47
 (
  ("(var3 down)" 0 2)
  ("(var3 stable)" 2 49)
  ("(var3 up)" 49 83)
  ("(var3 stable)" 83 299)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 80)
  ("(var4 stable)" 80 177)
  ("(var4 down)" 177 257)
  ("(var4 stable)" 257 299)
  ("(var1 stable)" 0 50)
  ("(var1 up)" 50 53)
  ("(var1 down)" 53 55)
  ("(var1 up)" 55 80)
  ("(var1 stable)" 80 299)
  ("(var2 stable)" 0 70)
  ("(var2 down)" 70 72)
  ("(var2 stable)" 72 105)
  ("(var2 up)" 105 173)
  ("(var2 down)" 173 176)
  ("(var2 up)" 176 178)
  ("(var2 stable)" 178 299)
 )
)
(48
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 88)
  ("(var3 stable)" 88 306)
  ("(var4 down)" 0 2)
  ("(var4 stable)" 2 55)
  ("(var4 up)" 55 85)
  ("(var4 down)" 85 87)
  ("(var4 up)" 87 89)
  ("(var4 stable)" 89 172)
  ("(var4 down)" 172 174)
  ("(var4 up)" 174 177)
  ("(var4 down)" 177 268)
  ("(var4 stable)" 268 306)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 57)
  ("(var1 stable)" 57 60)
  ("(var1 up)" 60 86)
  ("(var1 stable)" 86 306)
  ("(var2 stable)" 0 74)
  ("(var2 down)" 74 76)
  ("(var2 up)" 76 199)
  ("(var2 stable)" 199 306)
 )
)
(49
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 86)
  ("(var3 stable)" 86 335)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 86)
  ("(var4 stable)" 86 212)
  ("(var4 down)" 212 289)
  ("(var4 up)" 289 291)
  ("(var4 down)" 291 293)
  ("(var4 stable)" 293 335)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 54)
  ("(var1 stable)" 54 56)
  ("(var1 up)" 56 89)
  ("(var1 stable)" 89 335)
  ("(var2 stable)" 0 74)
  ("(var2 down)" 74 76)
  ("(var2 up)" 76 217)
  ("(var2 stable)" 217 335)
 )
)
(50
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 98)
  ("(var3 stable)" 98 333)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 102)
  ("(var4 stable)" 102 221)
  ("(var4 down)" 221 286)
  ("(var4 up)" 286 288)
  ("(var4 down)" 288 308)
  ("(var4 stable)" 308 333)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 102)
  ("(var1 stable)" 102 333)
  ("(var2 stable)" 0 90)
  ("(var2 down)" 90 92)
  ("(var2 stable)" 92 121)
  ("(var2 up)" 121 214)
  ("(var2 stable)" 214 333)
 )
)
(51
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 89)
  ("(var3 stable)" 89 334)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 97)
  ("(var4 stable)" 97 217)
  ("(var4 up)" 217 219)
  ("(var4 down)" 219 314)
  ("(var4 stable)" 314 334)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 96)
  ("(var1 stable)" 96 334)
  ("(var2 stable)" 0 82)
  ("(var2 down)" 82 84)
  ("(var2 stable)" 84 115)
  ("(var2 down)" 115 117)
  ("(var2 up)" 117 212)
  ("(var2 stable)" 212 334)
 )
)
(52
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 72)
  ("(var3 stable)" 72 319)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 76)
  ("(var4 stable)" 76 187)
  ("(var4 down)" 187 269)
  ("(var4 stable)" 269 319)
  ("(var1 stable)" 0 17)
  ("(var1 down)" 17 19)
  ("(var1 up)" 19 21)
  ("(var1 stable)" 21 45)
  ("(var1 up)" 45 74)
  ("(var1 down)" 74 76)
  ("(var1 stable)" 76 319)
  ("(var2 stable)" 0 64)
  ("(var2 down)" 64 66)
  ("(var2 stable)" 66 105)
  ("(var2 up)" 105 207)
  ("(var2 stable)" 207 319)
 )
)
(53
 (
  ("(var3 stable)" 0 95)
  ("(var3 up)" 95 97)
  ("(var3 stable)" 97 100)
  ("(var3 up)" 100 130)
  ("(var3 stable)" 130 367)
  ("(var4 stable)" 0 97)
  ("(var4 up)" 97 135)
  ("(var4 stable)" 135 236)
  ("(var4 down)" 236 322)
  ("(var4 stable)" 322 367)
  ("(var1 stable)" 0 94)
  ("(var1 up)" 94 130)
  ("(var1 stable)" 130 367)
  ("(var2 stable)" 0 118)
  ("(var2 down)" 118 120)
  ("(var2 up)" 120 219)
  ("(var2 stable)" 219 221)
  ("(var2 up)" 221 264)
  ("(var2 stable)" 264 367)
 )
)
(54
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 116)
  ("(var3 stable)" 116 342)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 114)
  ("(var4 stable)" 114 225)
  ("(var4 down)" 225 294)
  ("(var4 stable)" 294 342)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 116)
  ("(var1 stable)" 116 342)
  ("(var2 stable)" 0 106)
  ("(var2 down)" 106 108)
  ("(var2 up)" 108 233)
  ("(var2 stable)" 233 342)
 )
)
(55
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 69)
  ("(var3 stable)" 69 71)
  ("(var3 up)" 71 73)
  ("(var3 stable)" 73 325)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 74)
  ("(var4 stable)" 74 168)
  ("(var4 down)" 168 211)
  ("(var4 stable)" 211 216)
  ("(var4 down)" 216 270)
  ("(var4 up)" 270 272)
  ("(var4 down)" 272 274)
  ("(var4 stable)" 274 325)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 75)
  ("(var1 stable)" 75 325)
  ("(var2 stable)" 0 63)
  ("(var2 down)" 63 65)
  ("(var2 up)" 65 213)
  ("(var2 stable)" 213 325)
 )
)
(56
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 76)
  ("(var3 down)" 76 78)
  ("(var3 stable)" 78 298)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 75)
  ("(var4 stable)" 75 178)
  ("(var4 down)" 178 256)
  ("(var4 stable)" 256 298)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 77)
  ("(var1 stable)" 77 298)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 70)
  ("(var2 stable)" 70 94)
  ("(var2 up)" 94 184)
  ("(var2 stable)" 184 298)
 )
)
(57
 (
  ("(var3 stable)" 0 68)
  ("(var3 up)" 68 97)
  ("(var3 stable)" 97 321)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 100)
  ("(var4 down)" 100 102)
  ("(var4 stable)" 102 107)
  ("(var4 up)" 107 109)
  ("(var4 stable)" 109 189)
  ("(var4 down)" 189 313)
  ("(var4 up)" 313 315)
  ("(var4 down)" 315 318)
  ("(var4 up)" 318 321)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 98)
  ("(var1 stable)" 98 321)
  ("(var2 up)" 0 2)
  ("(var2 stable)" 2 89)
  ("(var2 down)" 89 91)
  ("(var2 up)" 91 213)
  ("(var2 stable)" 213 321)
 )
)
(58
 (
  ("(var3 up)" 0 2)
  ("(var3 down)" 2 4)
  ("(var3 stable)" 4 47)
  ("(var3 up)" 47 49)
  ("(var3 down)" 49 51)
  ("(var3 up)" 51 53)
  ("(var3 stable)" 53 56)
  ("(var3 up)" 56 85)
  ("(var3 stable)" 85 332)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 91)
  ("(var4 stable)" 91 196)
  ("(var4 down)" 196 290)
  ("(var4 up)" 290 293)
  ("(var4 stable)" 293 332)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 53)
  ("(var1 stable)" 53 58)
  ("(var1 up)" 58 83)
  ("(var1 stable)" 83 332)
  ("(var2 stable)" 0 76)
  ("(var2 down)" 76 78)
  ("(var2 up)" 78 183)
  ("(var2 down)" 183 185)
  ("(var2 up)" 185 196)
  ("(var2 stable)" 196 332)
 )
)
(59
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 111)
  ("(var3 stable)" 111 332)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 74)
  ("(var4 stable)" 74 77)
  ("(var4 up)" 77 119)
  ("(var4 stable)" 119 195)
  ("(var4 down)" 195 298)
  ("(var4 stable)" 298 332)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 114)
  ("(var1 stable)" 114 332)
  ("(var2 stable)" 0 102)
  ("(var2 down)" 102 106)
  ("(var2 up)" 106 234)
  ("(var2 stable)" 234 332)
 )
)
(60
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 104)
  ("(var3 stable)" 104 350)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 74)
  ("(var4 stable)" 74 76)
  ("(var4 up)" 76 108)
  ("(var4 stable)" 108 200)
  ("(var4 down)" 200 335)
  ("(var4 up)" 335 337)
  ("(var4 down)" 337 339)
  ("(var4 stable)" 339 343)
  ("(var4 down)" 343 347)
  ("(var4 up)" 347 350)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 108)
  ("(var1 stable)" 108 350)
  ("(var2 stable)" 0 93)
  ("(var2 down)" 93 95)
  ("(var2 up)" 95 213)
  ("(var2 stable)" 213 350)
 )
)
(61
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 69)
  ("(var3 stable)" 69 300)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 40)
  ("(var4 stable)" 40 43)
  ("(var4 up)" 43 74)
  ("(var4 stable)" 74 167)
  ("(var4 down)" 167 257)
  ("(var4 stable)" 257 300)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 74)
  ("(var1 stable)" 74 300)
  ("(var2 stable)" 0 60)
  ("(var2 down)" 60 64)
  ("(var2 up)" 64 189)
  ("(var2 down)" 189 191)
  ("(var2 up)" 191 193)
  ("(var2 stable)" 193 300)
 )
)
(62
 (
  ("(var3 stable)" 0 96)
  ("(var3 down)" 96 98)
  ("(var3 up)" 98 127)
  ("(var3 down)" 127 129)
  ("(var3 stable)" 129 382)
  ("(var4 stable)" 0 97)
  ("(var4 up)" 97 122)
  ("(var4 down)" 122 124)
  ("(var4 up)" 124 138)
  ("(var4 stable)" 138 253)
  ("(var4 down)" 253 332)
  ("(var4 up)" 332 334)
  ("(var4 down)" 334 339)
  ("(var4 stable)" 339 382)
  ("(var1 stable)" 0 96)
  ("(var1 up)" 96 130)
  ("(var1 stable)" 130 382)
  ("(var2 stable)" 0 116)
  ("(var2 down)" 116 118)
  ("(var2 up)" 118 222)
  ("(var2 stable)" 222 224)
  ("(var2 up)" 224 255)
  ("(var2 stable)" 255 382)
 )
)
(63
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 76)
  ("(var3 stable)" 76 313)
  ("(var4 stable)" 0 48)
  ("(var4 up)" 48 92)
  ("(var4 stable)" 92 177)
  ("(var4 down)" 177 276)
  ("(var4 stable)" 276 313)
  ("(var1 stable)" 0 47)
  ("(var1 up)" 47 76)
  ("(var1 stable)" 76 313)
  ("(var2 stable)" 0 67)
  ("(var2 down)" 67 71)
  ("(var2 up)" 71 192)
  ("(var2 stable)" 192 313)
 )
)
(64
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 62)
  ("(var3 stable)" 62 301)
  ("(var4 stable)" 0 29)
  ("(var4 up)" 29 67)
  ("(var4 stable)" 67 158)
  ("(var4 down)" 158 255)
  ("(var4 stable)" 255 299)
  ("(var4 up)" 299 301)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 30)
  ("(var1 up)" 30 64)
  ("(var1 stable)" 64 301)
  ("(var2 stable)" 0 53)
  ("(var2 down)" 53 55)
  ("(var2 up)" 55 198)
  ("(var2 stable)" 198 301)
 )
)
(65
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 97)
  ("(var3 stable)" 97 326)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 89)
  ("(var4 down)" 89 91)
  ("(var4 stable)" 91 192)
  ("(var4 down)" 192 282)
  ("(var4 up)" 282 284)
  ("(var4 down)" 284 286)
  ("(var4 stable)" 286 326)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 90)
  ("(var1 stable)" 90 326)
  ("(var2 stable)" 0 79)
  ("(var2 down)" 79 83)
  ("(var2 up)" 83 185)
  ("(var2 stable)" 185 326)
 )
)
(66
 (
  ("(var3 stable)" 0 45)
  ("(var3 up)" 45 47)
  ("(var3 stable)" 47 50)
  ("(var3 up)" 50 75)
  ("(var3 stable)" 75 302)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 49)
  ("(var4 stable)" 49 51)
  ("(var4 up)" 51 83)
  ("(var4 stable)" 83 164)
  ("(var4 down)" 164 249)
  ("(var4 stable)" 249 251)
  ("(var4 down)" 251 261)
  ("(var4 stable)" 261 300)
  ("(var4 up)" 300 302)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 77)
  ("(var1 stable)" 77 302)
  ("(var2 stable)" 0 66)
  ("(var2 down)" 66 70)
  ("(var2 up)" 70 185)
  ("(var2 stable)" 185 302)
 )
)
(67
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 62)
  ("(var3 down)" 62 64)
  ("(var3 up)" 64 92)
  ("(var3 stable)" 92 308)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 95)
  ("(var4 stable)" 95 178)
  ("(var4 down)" 178 283)
  ("(var4 stable)" 283 308)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 93)
  ("(var1 stable)" 93 308)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 85)
  ("(var2 up)" 85 126)
  ("(var2 down)" 126 128)
  ("(var2 up)" 128 205)
  ("(var2 stable)" 205 308)
 )
)
(68
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 109)
  ("(var3 stable)" 109 336)
  ("(var4 up)" 0 2)
  ("(var4 stable)" 2 77)
  ("(var4 up)" 77 111)
  ("(var4 stable)" 111 229)
  ("(var4 down)" 229 300)
  ("(var4 stable)" 300 336)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 111)
  ("(var1 stable)" 111 336)
  ("(var2 stable)" 0 100)
  ("(var2 down)" 100 104)
  ("(var2 up)" 104 237)
  ("(var2 stable)" 237 333)
  ("(var2 down)" 333 336)
 )
)
(69
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 69)
  ("(var3 stable)" 69 300)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 77)
  ("(var4 stable)" 77 163)
  ("(var4 down)" 163 255)
  ("(var4 stable)" 255 300)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 71)
  ("(var1 stable)" 71 73)
  ("(var1 up)" 73 75)
  ("(var1 stable)" 75 300)
  ("(var2 stable)" 0 59)
  ("(var2 down)" 59 61)
  ("(var2 up)" 61 200)
  ("(var2 stable)" 200 300)
 )
)
(70
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 84)
  ("(var3 stable)" 84 301)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 83)
  ("(var4 down)" 83 85)
  ("(var4 stable)" 85 200)
  ("(var4 down)" 200 204)
  ("(var4 stable)" 204 206)
  ("(var4 down)" 206 258)
  ("(var4 stable)" 258 299)
  ("(var4 up)" 299 301)
  ("(var1 stable)" 0 45)
  ("(var1 up)" 45 83)
  ("(var1 stable)" 83 301)
  ("(var2 stable)" 0 73)
  ("(var2 down)" 73 75)
  ("(var2 up)" 75 180)
  ("(var2 stable)" 180 301)
 )
)
(71
 (
  ("(var3 stable)" 0 75)
  ("(var3 up)" 75 112)
  ("(var3 stable)" 112 362)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 73)
  ("(var4 stable)" 73 77)
  ("(var4 up)" 77 108)
  ("(var4 stable)" 108 215)
  ("(var4 down)" 215 239)
  ("(var4 up)" 239 241)
  ("(var4 down)" 241 319)
  ("(var4 stable)" 319 362)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 109)
  ("(var1 stable)" 109 362)
  ("(var2 stable)" 0 95)
  ("(var2 down)" 95 99)
  ("(var2 up)" 99 245)
  ("(var2 stable)" 245 362)
 )
)
(72
 (
  ("(var3 stable)" 0 52)
  ("(var3 up)" 52 77)
  ("(var3 stable)" 77 307)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 82)
  ("(var4 stable)" 82 171)
  ("(var4 down)" 171 196)
  ("(var4 stable)" 196 200)
  ("(var4 down)" 200 261)
  ("(var4 stable)" 261 263)
  ("(var4 down)" 263 266)
  ("(var4 stable)" 266 302)
  ("(var4 down)" 302 307)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 83)
  ("(var1 stable)" 83 307)
  ("(var2 stable)" 0 72)
  ("(var2 down)" 72 74)
  ("(var2 up)" 74 196)
  ("(var2 stable)" 196 307)
 )
)
(73
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 102)
  ("(var3 stable)" 102 355)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 107)
  ("(var4 down)" 107 109)
  ("(var4 stable)" 109 209)
  ("(var4 down)" 209 331)
  ("(var4 stable)" 331 355)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 98)
  ("(var1 stable)" 98 355)
  ("(var2 stable)" 0 88)
  ("(var2 down)" 88 92)
  ("(var2 stable)" 92 108)
  ("(var2 up)" 108 226)
  ("(var2 down)" 226 228)
  ("(var2 up)" 228 231)
  ("(var2 stable)" 231 234)
  ("(var2 up)" 234 236)
  ("(var2 stable)" 236 355)
 )
)
(74
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 85)
  ("(var3 stable)" 85 344)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 92)
  ("(var4 stable)" 92 192)
  ("(var4 down)" 192 194)
  ("(var4 stable)" 194 196)
  ("(var4 down)" 196 198)
  ("(var4 up)" 198 201)
  ("(var4 down)" 201 302)
  ("(var4 stable)" 302 344)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 88)
  ("(var1 stable)" 88 344)
  ("(var2 stable)" 0 79)
  ("(var2 down)" 79 81)
  ("(var2 stable)" 81 116)
  ("(var2 up)" 116 118)
  ("(var2 stable)" 118 124)
  ("(var2 up)" 124 182)
  ("(var2 down)" 182 184)
  ("(var2 up)" 184 223)
  ("(var2 stable)" 223 344)
 )
)
(75
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 77)
  ("(var3 stable)" 77 308)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 79)
  ("(var4 stable)" 79 192)
  ("(var4 down)" 192 194)
  ("(var4 up)" 194 196)
  ("(var4 down)" 196 270)
  ("(var4 stable)" 270 308)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 44)
  ("(var1 up)" 44 82)
  ("(var1 stable)" 82 308)
  ("(var2 stable)" 0 68)
  ("(var2 down)" 68 70)
  ("(var2 up)" 70 180)
  ("(var2 stable)" 180 308)
 )
)
(76
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 58)
  ("(var3 down)" 58 60)
  ("(var3 up)" 60 89)
  ("(var3 stable)" 89 336)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 91)
  ("(var4 stable)" 91 188)
  ("(var4 up)" 188 190)
  ("(var4 down)" 190 284)
  ("(var4 up)" 284 286)
  ("(var4 stable)" 286 334)
  ("(var4 down)" 334 336)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 96)
  ("(var1 stable)" 96 336)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 83)
  ("(var2 up)" 83 180)
  ("(var2 down)" 180 182)
  ("(var2 up)" 182 218)
  ("(var2 down)" 218 220)
  ("(var2 up)" 220 222)
  ("(var2 stable)" 222 336)
 )
)
(77
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 84)
  ("(var3 stable)" 84 339)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 86)
  ("(var4 down)" 86 88)
  ("(var4 up)" 88 90)
  ("(var4 stable)" 90 212)
  ("(var4 down)" 212 214)
  ("(var4 stable)" 214 218)
  ("(var4 down)" 218 290)
  ("(var4 stable)" 290 339)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 48)
  ("(var1 up)" 48 90)
  ("(var1 stable)" 90 339)
  ("(var2 stable)" 0 74)
  ("(var2 down)" 74 76)
  ("(var2 up)" 76 216)
  ("(var2 down)" 216 218)
  ("(var2 stable)" 218 339)
 )
)
(78
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 58)
  ("(var3 stable)" 58 64)
  ("(var3 up)" 64 93)
  ("(var3 stable)" 93 342)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 93)
  ("(var4 stable)" 93 188)
  ("(var4 down)" 188 296)
  ("(var4 stable)" 296 342)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 60)
  ("(var1 down)" 60 62)
  ("(var1 up)" 62 95)
  ("(var1 stable)" 95 97)
  ("(var1 up)" 97 99)
  ("(var1 stable)" 99 342)
  ("(var2 stable)" 0 81)
  ("(var2 down)" 81 88)
  ("(var2 stable)" 88 105)
  ("(var2 up)" 105 125)
  ("(var2 stable)" 125 127)
  ("(var2 up)" 127 220)
  ("(var2 stable)" 220 342)
 )
)
(79
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 41)
  ("(var3 stable)" 41 45)
  ("(var3 up)" 45 71)
  ("(var3 stable)" 71 303)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 75)
  ("(var4 stable)" 75 161)
  ("(var4 down)" 161 163)
  ("(var4 up)" 163 165)
  ("(var4 down)" 165 269)
  ("(var4 stable)" 269 303)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 73)
  ("(var1 stable)" 73 303)
  ("(var2 stable)" 0 62)
  ("(var2 down)" 62 64)
  ("(var2 up)" 64 163)
  ("(var2 stable)" 163 166)
  ("(var2 up)" 166 202)
  ("(var2 stable)" 202 303)
 )
)
(80
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 42)
  ("(var3 down)" 42 44)
  ("(var3 up)" 44 68)
  ("(var3 stable)" 68 293)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 80)
  ("(var4 stable)" 80 157)
  ("(var4 down)" 157 245)
  ("(var4 up)" 245 247)
  ("(var4 down)" 247 252)
  ("(var4 stable)" 252 293)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 77)
  ("(var1 stable)" 77 293)
  ("(var2 stable)" 0 61)
  ("(var2 down)" 61 63)
  ("(var2 up)" 63 93)
  ("(var2 down)" 93 95)
  ("(var2 up)" 95 194)
  ("(var2 stable)" 194 293)
 )
)
(81
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 98)
  ("(var3 stable)" 98 329)
  ("(var4 stable)" 0 62)
  ("(var4 up)" 62 65)
  ("(var4 down)" 65 67)
  ("(var4 up)" 67 104)
  ("(var4 stable)" 104 190)
  ("(var4 down)" 190 303)
  ("(var4 stable)" 303 329)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 93)
  ("(var1 stable)" 93 329)
  ("(var2 stable)" 0 84)
  ("(var2 down)" 84 86)
  ("(var2 stable)" 86 120)
  ("(var2 up)" 120 217)
  ("(var2 stable)" 217 329)
 )
)
(82
 (
  ("(var3 stable)" 0 74)
  ("(var3 up)" 74 101)
  ("(var3 stable)" 101 326)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 100)
  ("(var4 stable)" 100 196)
  ("(var4 down)" 196 283)
  ("(var4 up)" 283 285)
  ("(var4 down)" 285 287)
  ("(var4 stable)" 287 326)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 101)
  ("(var1 stable)" 101 326)
  ("(var2 stable)" 0 91)
  ("(var2 down)" 91 93)
  ("(var2 up)" 93 206)
  ("(var2 down)" 206 209)
  ("(var2 stable)" 209 326)
 )
)
(83
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 93)
  ("(var3 stable)" 93 312)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 97)
  ("(var4 stable)" 97 207)
  ("(var4 down)" 207 275)
  ("(var4 stable)" 275 312)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 95)
  ("(var1 stable)" 95 312)
  ("(var2 stable)" 0 83)
  ("(var2 down)" 83 85)
  ("(var2 stable)" 85 117)
  ("(var2 up)" 117 211)
  ("(var2 down)" 211 213)
  ("(var2 stable)" 213 312)
 )
)
(84
 (
  ("(var3 stable)" 0 47)
  ("(var3 up)" 47 77)
  ("(var3 stable)" 77 80)
  ("(var3 up)" 80 82)
  ("(var3 stable)" 82 293)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 78)
  ("(var4 stable)" 78 153)
  ("(var4 down)" 153 260)
  ("(var4 stable)" 260 293)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 74)
  ("(var1 stable)" 74 293)
  ("(var2 stable)" 0 67)
  ("(var2 down)" 67 69)
  ("(var2 stable)" 69 100)
  ("(var2 up)" 100 187)
  ("(var2 stable)" 187 293)
 )
)
(85
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 78)
  ("(var3 down)" 78 80)
  ("(var3 up)" 80 83)
  ("(var3 stable)" 83 331)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 76)
  ("(var4 down)" 76 79)
  ("(var4 up)" 79 81)
  ("(var4 stable)" 81 180)
  ("(var4 down)" 180 277)
  ("(var4 stable)" 277 280)
  ("(var4 down)" 280 284)
  ("(var4 stable)" 284 331)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 37)
  ("(var1 down)" 37 39)
  ("(var1 up)" 39 80)
  ("(var1 stable)" 80 331)
  ("(var2 stable)" 0 67)
  ("(var2 down)" 67 71)
  ("(var2 stable)" 71 97)
  ("(var2 up)" 97 211)
  ("(var2 stable)" 211 331)
 )
)
(86
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 77)
  ("(var3 stable)" 77 313)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 72)
  ("(var4 stable)" 72 166)
  ("(var4 down)" 166 277)
  ("(var4 stable)" 277 313)
  ("(var1 stable)" 0 33)
  ("(var1 down)" 33 35)
  ("(var1 up)" 35 67)
  ("(var1 stable)" 67 313)
  ("(var2 stable)" 0 59)
  ("(var2 down)" 59 61)
  ("(var2 stable)" 61 96)
  ("(var2 up)" 96 204)
  ("(var2 stable)" 204 313)
 )
)
(87
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 73)
  ("(var3 stable)" 73 310)
  ("(var4 stable)" 0 43)
  ("(var4 up)" 43 72)
  ("(var4 stable)" 72 74)
  ("(var4 up)" 74 76)
  ("(var4 stable)" 76 179)
  ("(var4 down)" 179 262)
  ("(var4 up)" 262 264)
  ("(var4 down)" 264 266)
  ("(var4 stable)" 266 310)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 72)
  ("(var1 stable)" 72 310)
  ("(var2 stable)" 0 61)
  ("(var2 down)" 61 63)
  ("(var2 stable)" 63 98)
  ("(var2 up)" 98 197)
  ("(var2 down)" 197 199)
  ("(var2 stable)" 199 310)
 )
)
(88
 (
  ("(var3 stable)" 0 82)
  ("(var3 up)" 82 84)
  ("(var3 stable)" 84 86)
  ("(var3 up)" 86 116)
  ("(var3 stable)" 116 366)
  ("(var4 stable)" 0 83)
  ("(var4 up)" 83 112)
  ("(var4 stable)" 112 219)
  ("(var4 down)" 219 221)
  ("(var4 up)" 221 223)
  ("(var4 down)" 223 246)
  ("(var4 up)" 246 248)
  ("(var4 down)" 248 321)
  ("(var4 stable)" 321 366)
  ("(var1 stable)" 0 84)
  ("(var1 up)" 84 118)
  ("(var1 stable)" 118 366)
  ("(var2 stable)" 0 105)
  ("(var2 down)" 105 107)
  ("(var2 stable)" 107 140)
  ("(var2 up)" 140 152)
  ("(var2 down)" 152 154)
  ("(var2 up)" 154 200)
  ("(var2 down)" 200 202)
  ("(var2 up)" 202 210)
  ("(var2 down)" 210 212)
  ("(var2 up)" 212 251)
  ("(var2 stable)" 251 366)
 )
)
(89
 (
  ("(var3 stable)" 0 42)
  ("(var3 up)" 42 69)
  ("(var3 stable)" 69 305)
  ("(var4 stable)" 0 36)
  ("(var4 up)" 36 38)
  ("(var4 down)" 38 40)
  ("(var4 up)" 40 73)
  ("(var4 stable)" 73 162)
  ("(var4 down)" 162 261)
  ("(var4 stable)" 261 305)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 77)
  ("(var1 stable)" 77 305)
  ("(var2 stable)" 0 62)
  ("(var2 down)" 62 64)
  ("(var2 up)" 64 106)
  ("(var2 stable)" 106 108)
  ("(var2 up)" 108 194)
  ("(var2 stable)" 194 305)
 )
)
(90
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 89)
  ("(var3 stable)" 89 91)
  ("(var3 up)" 91 103)
  ("(var3 stable)" 103 348)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 100)
  ("(var4 stable)" 100 180)
  ("(var4 down)" 180 182)
  ("(var4 up)" 182 184)
  ("(var4 stable)" 184 225)
  ("(var4 down)" 225 290)
  ("(var4 stable)" 290 293)
  ("(var4 down)" 293 299)
  ("(var4 stable)" 299 348)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 100)
  ("(var1 stable)" 100 348)
  ("(var2 stable)" 0 87)
  ("(var2 down)" 87 91)
  ("(var2 stable)" 91 126)
  ("(var2 up)" 126 228)
  ("(var2 stable)" 228 348)
 )
)
(91
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 66)
  ("(var3 stable)" 66 302)
  ("(var4 stable)" 0 34)
  ("(var4 up)" 34 36)
  ("(var4 stable)" 36 40)
  ("(var4 up)" 40 69)
  ("(var4 stable)" 69 185)
  ("(var4 down)" 185 256)
  ("(var4 stable)" 256 299)
  ("(var4 down)" 299 302)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 68)
  ("(var1 stable)" 68 302)
  ("(var2 stable)" 0 56)
  ("(var2 down)" 56 58)
  ("(var2 up)" 58 187)
  ("(var2 stable)" 187 302)
 )
)
(92
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 101)
  ("(var3 stable)" 101 345)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 103)
  ("(var4 down)" 103 105)
  ("(var4 up)" 105 107)
  ("(var4 down)" 107 109)
  ("(var4 stable)" 109 205)
  ("(var4 down)" 205 242)
  ("(var4 up)" 242 244)
  ("(var4 down)" 244 312)
  ("(var4 stable)" 312 345)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 99)
  ("(var1 stable)" 99 101)
  ("(var1 up)" 101 103)
  ("(var1 stable)" 103 345)
  ("(var2 stable)" 0 92)
  ("(var2 down)" 92 94)
  ("(var2 up)" 94 234)
  ("(var2 stable)" 234 345)
 )
)
(93
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 79)
  ("(var3 stable)" 79 312)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 75)
  ("(var4 stable)" 75 77)
  ("(var4 up)" 77 80)
  ("(var4 stable)" 80 197)
  ("(var4 down)" 197 269)
  ("(var4 up)" 269 271)
  ("(var4 down)" 271 273)
  ("(var4 stable)" 273 312)
  ("(var1 stable)" 0 44)
  ("(var1 up)" 44 82)
  ("(var1 stable)" 82 312)
  ("(var2 stable)" 0 69)
  ("(var2 down)" 69 71)
  ("(var2 up)" 71 197)
  ("(var2 stable)" 197 312)
 )
)
(94
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 78)
  ("(var3 stable)" 78 80)
  ("(var3 up)" 80 110)
  ("(var3 stable)" 110 354)
  ("(var4 stable)" 0 74)
  ("(var4 up)" 74 115)
  ("(var4 stable)" 115 205)
  ("(var4 down)" 205 318)
  ("(var4 stable)" 318 354)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 108)
  ("(var1 stable)" 108 354)
  ("(var2 stable)" 0 98)
  ("(var2 down)" 98 100)
  ("(var2 up)" 100 231)
  ("(var2 stable)" 231 354)
 )
)
(95
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 42)
  ("(var3 down)" 42 44)
  ("(var3 up)" 44 87)
  ("(var3 stable)" 87 332)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 95)
  ("(var4 stable)" 95 213)
  ("(var4 down)" 213 285)
  ("(var4 stable)" 285 327)
  ("(var4 up)" 327 332)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 55)
  ("(var1 down)" 55 57)
  ("(var1 up)" 57 85)
  ("(var1 stable)" 85 87)
  ("(var1 up)" 87 90)
  ("(var1 stable)" 90 332)
  ("(var2 stable)" 0 76)
  ("(var2 down)" 76 80)
  ("(var2 up)" 80 224)
  ("(var2 stable)" 224 332)
 )
)
(96
 (
  ("(var3 up)" 0 3)
  ("(var3 stable)" 3 44)
  ("(var3 up)" 44 67)
  ("(var3 stable)" 67 69)
  ("(var3 up)" 69 71)
  ("(var3 stable)" 71 326)
  ("(var4 up)" 0 2)
  ("(var4 stable)" 2 35)
  ("(var4 up)" 35 67)
  ("(var4 stable)" 67 69)
  ("(var4 up)" 69 75)
  ("(var4 stable)" 75 77)
  ("(var4 up)" 77 79)
  ("(var4 down)" 79 83)
  ("(var4 up)" 83 85)
  ("(var4 stable)" 85 87)
  ("(var4 up)" 87 89)
  ("(var4 stable)" 89 183)
  ("(var4 down)" 183 186)
  ("(var4 up)" 186 188)
  ("(var4 down)" 188 219)
  ("(var4 up)" 219 221)
  ("(var4 down)" 221 276)
  ("(var4 stable)" 276 323)
  ("(var4 down)" 323 326)
  ("(var1 stable)" 0 39)
  ("(var1 up)" 39 78)
  ("(var1 stable)" 78 326)
  ("(var2 down)" 0 2)
  ("(var2 stable)" 2 61)
  ("(var2 down)" 61 65)
  ("(var2 up)" 65 107)
  ("(var2 down)" 107 110)
  ("(var2 up)" 110 169)
  ("(var2 down)" 169 171)
  ("(var2 up)" 171 206)
  ("(var2 stable)" 206 326)
 )
)
(97
 (
  ("(var3 stable)" 0 3)
  ("(var3 down)" 3 5)
  ("(var3 stable)" 5 80)
  ("(var3 up)" 80 107)
  ("(var3 stable)" 107 365)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 119)
  ("(var4 stable)" 119 243)
  ("(var4 down)" 243 245)
  ("(var4 up)" 245 247)
  ("(var4 down)" 247 325)
  ("(var4 up)" 325 327)
  ("(var4 down)" 327 329)
  ("(var4 stable)" 329 365)
  ("(var1 stable)" 0 74)
  ("(var1 down)" 74 76)
  ("(var1 up)" 76 111)
  ("(var1 stable)" 111 365)
  ("(var2 stable)" 0 101)
  ("(var2 down)" 101 105)
  ("(var2 up)" 105 243)
  ("(var2 stable)" 243 245)
  ("(var2 up)" 245 247)
  ("(var2 stable)" 247 365)
 )
)
(98
 (
  ("(var3 stable)" 0 34)
  ("(var3 up)" 34 36)
  ("(var3 stable)" 36 38)
  ("(var3 up)" 38 61)
  ("(var3 stable)" 61 276)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 63)
  ("(var4 stable)" 63 140)
  ("(var4 down)" 140 143)
  ("(var4 up)" 143 145)
  ("(var4 down)" 145 229)
  ("(var4 stable)" 229 231)
  ("(var4 down)" 231 233)
  ("(var4 stable)" 233 276)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 63)
  ("(var1 stable)" 63 276)
  ("(var2 stable)" 0 51)
  ("(var2 down)" 51 53)
  ("(var2 stable)" 53 81)
  ("(var2 up)" 81 174)
  ("(var2 stable)" 174 276)
 )
)
(99
 (
  ("(var3 stable)" 0 40)
  ("(var3 up)" 40 72)
  ("(var3 stable)" 72 76)
  ("(var3 up)" 76 78)
  ("(var3 stable)" 78 307)
  ("(var4 stable)" 0 42)
  ("(var4 up)" 42 74)
  ("(var4 stable)" 74 189)
  ("(var4 down)" 189 261)
  ("(var4 stable)" 261 307)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 75)
  ("(var1 stable)" 75 307)
  ("(var2 stable)" 0 62)
  ("(var2 down)" 62 64)
  ("(var2 stable)" 64 102)
  ("(var2 up)" 102 195)
  ("(var2 down)" 195 197)
  ("(var2 stable)" 197 307)
 )
)
(100
 (
  ("(var3 stable)" 0 65)
  ("(var3 up)" 65 97)
  ("(var3 stable)" 97 300)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 93)
  ("(var4 stable)" 93 175)
  ("(var4 down)" 175 263)
  ("(var4 up)" 263 265)
  ("(var4 down)" 265 268)
  ("(var4 stable)" 268 270)
  ("(var4 down)" 270 272)
  ("(var4 stable)" 272 300)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 93)
  ("(var1 stable)" 93 300)
  ("(var2 stable)" 0 84)
  ("(var2 down)" 84 86)
  ("(var2 up)" 86 201)
  ("(var2 stable)" 201 300)
 )
)
